A:Type, F:(A), L:(A List). (k:A. Dec(F(k)))  Dec((kL.F(k))) 

latex

Definitions	x:A. B(x), , P  Q, x(s), t  T, list_accum(x,a.f(x;a);y;l), Y, A, A c B, Dec(P), Top, S  T, P  Q, False, x. t(x), A  B, {i..j}, i  j < k, P & Q, (xL.P(x)), x:A. B(x), (x  l), ||as||, i  j , t  ...$L, P  Q, P  Q, l[i], hd(l), nth_tl(n;as), if b then t else f fi , i z j, b, i <z j, tt, ff, , T, True, as @ bs, Unit
Lemmas	decidable wf, append-nil, top wf, false wf, l exists wf, nat wf, length wf1, int seg wf, not wf, select wf, le wf, append wf, l member wf, length nil, length cons, non neg length, length append, select append front, select append back, decidable lt, squash wf, true wf, append assoc sq, length wf2